a, b:. GCD(a;b;gcd(a;b)) 

latex

Definitions	|i|, , AB, A, False, GCD(a;b;y), ij, P  Q, Prop, x:A. B(x), t  T, Unit, P  Q, P & Q, i=j, , b, b, a  b, , P  Q, T, gcd(a;b), True
Lemmas	gcd p sym, gcd wf, divide wfa, gcd p shift, rem to div, true wf, squash wf, nequal wf, rem bounds z, gcd p wf, gcd p zero, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, absval wf, nat wf, nat properties, ge wf, le wf